M:MsgA. ma-is-empty(M)  M =  

latex

Definitions	MsgA, t  T, , Prop, b, x:A. B(x), ma-is-empty(M), P  Q, P  Q, P & Q, P  Q, p  q, Id, ||as||, a:A fp B(a), Top, if b t else f fi, 1of(t), i=j, Knd, IdLnk, Valtype(da;k), fpf-is-empty(f), , x. t(x), State(ds), f(x)?z, rcv(l,tg), 2of(t), locl(a), KindDeq, IdDeq, True, T, mk-ma, S  T, , s = t,
Lemmas	ma-is-empty wf, mk-ma wf, squash wf, true wf, assert-fpf-is-empty, locl wf, id-deq wf, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, fpf wf, top wf, fpf-trivial-subtype-top, IdLnk wf, Knd wf, eq int wf, length wf1, Id wf, iff transitivity, and functionality wrt iff, assert of band, band wf, assert wf, ma-empty wf, msga wf